$\forall$$A$:Realizer, $i$:Id. $\neg$R{-}has{-}loc($A$;$i$) $\Rightarrow$ R{-}ds($A$;$i$) $=$  $\in$ $x$:Id fp$\rightarrow$ Type